\begin{tabbing}
antecedent{-}surjection(${\it es}$;$P$;$Q$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=antecedent{-}function(${\it es}$;$P$;$Q$;$f$)\+
\\[0ex]\& ($\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $Q$($e$)\} . $\exists$${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$($e$)\} . ($f$(${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$)))
\-
\end{tabbing}